M:Dsys. interface-compatible(M;) 

latex

Definitions	, interface-compatible(A;B), interface-link(A;B;l;tg), , rcv(l,tg) declared in M, mk-ma, KindDeq, False, P & Q, Prop, A, b, x  dom(f), rcv(l,tg), Id, IdLnk, Dsys, P  Q, source(l), destination(l), 1of(t), MsgA, Valtype(da;k), a:A fp B(a), x. t(x), x:A. B(x), t  T, Knd
Lemmas	Knd wf, fpf-trivial-subtype-top, ldst wf, msga wf, lsrc wf, IdLnk wf, Id wf, fpf-dom wf, assert wf, not wf, false wf, rcv wf, Kind-deq wf, dsys wf